2018-06-09

Гомотопические (Ко)-Лимиты

Как известно понять теорию категорий можно только если научился строить лимиты, а понять теорию гомотопий можно, если научился строить гомотопические лимиты! Гомотопический лимит в общем случае не равен категорному. Определение лимита простое — для любых f: A -> C и g: B -> C это ∑ (a: A) ∑ (b: B) f(a) =_C f(b) . Т.е. гомотопический лимит это обобщение расслоения. Кроме Кубической Теории Типов есть еще и Кубическая Гомотопическая теория, в которй 0-клетки — это пространства, 1-клетки — это расслоения, 2-клетки — это лимиты и колимиты, и т.д. В учебнике HoTT троллят читателя и вместо того, чтобы дать пулбеки и пушауты главами, пулбек предлагают решить как упражнение 2.11 ко второй главе.

Чтобы определить гомотопический колимит или пушаут, уже недостаточно пи и сигмы даже чтобы записать сигнатуру, нужны либо высшие индуктивные типы, либо, если вы умеете (а я вам рассказывал), ипредикативную кодировку. Проще говоря, нужно умножение в лимите заменить на сумму. Покажем как выглядит гомотопический колимит, это для функций f: C -> A, g: C -> B по сути сумма типов po1: A -> colim, po2: B -> colim и их равенства po3: (c: C) -> po1 (f c) = po2 (g c). Нужно построить для этого типа рекурсор и индукцию, кто возьмется?

Homotopy Colimit


 data pushout (A B C: U) (f: C -> A) (g: C -> B)
      = po1 (_: A)
      | po2 (_: B)
      | po3 (c: C) <i> [ (i=0) -> po1 (f c),
                         (i=1) -> po2 (g c) ]

Homotopy Limit


 pullback (A B C:U) (f: A -> C) (g: B -> C): U
    = (a: A)
    * (b: B)
    * Path C (f a) (g b)

 pb1 (A B C: U) (f: A -> C) (g: B -> C): pullback A B C f g -> A
   = \(x: pullback A B C f g) -> x.1
 pb2 (A B C: U) (f: A -> C) (g: B -> C): pullback A B C f g -> B
   = \(x: pullback A B C f g) -> x.2.1
 pb3 (A B C: U) (f: A -> C) (g: B -> C): (x: pullback A B C f g)
  -> Path C (f x.1) (g x.2.1)
   = \(x: pullback A B C f g) -> x.2.2

 induced (Z A B C: U) (f: A -> C) (g: B -> C)
         (z1: Z -> A) (z2: Z -> B)
         (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z))
       : Z -> pullback A B C f g
       = \(z: Z) -> ((z1 z),(z2 z),h z)

 pullbackSq (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B): U
          = (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z))
          * isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

 isPullbackSq (Z A B C: U) (f: A -> C) (g: B -> C) (z1: Z -> A) (z2: Z -> B)
              (h: (z:Z) -> Path C ((o Z A C f z1) z) (((o Z B C g z2)) z)): U
            = isEquiv Z (pullback A B C f g) (induced Z A B C f g z1 z2 h)

Exercise 2.11. Prove that the pullback P :≡ A x_C B defined in (2.15.11) is the corner of a pullback square.


completePullback (A B C: U) (f: A -> C) (g: B -> C)
    : pullbackSq (pullback A B C f g) A B C f g (pb1 A B C f g) (pb2 A B C f g)
    = ?

[1]. B.Munson. Cubical Homotopy Theory.
[2]. M.Frankland. Homotopy Theory Homotopy pullbacks
[3]. Infinity.HIT.Pullback
[4]. Homotopy Limits